Iof proof for Lemma bool cases sqequal:
((inr 
) ~ (inl )) 
((inr ) ~ (inr ))
by ((Sel 2 (D 0))
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term)))
C.| 12,41 |
((inr ) ~ (inl )) ((inr ) ~ (inr ))
by ((Sel 2 (D 0))
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term)))
C.
| Definitions |  T Q |